T:Type, as:(T List), f,g:(T).
((isl(priority-select(f; g; as))))  l_all(as; T; a.((((f(a))))  (((g(a)))))) 

latex

Definitions	Unit, t  T, , x:A. B(x), priority-select(f; g; as), P  Q, isl(x), b, A, , prop{i:l}, P  Q, x. t(x), l_all(L; T; x.P(x)), P  Q, P  Q, True, False
Lemmas	false wf, iff functionality wrt iff, priority-select-inr, l all wf, it wf, not wf, assert wf, isl wf, priority-select wf, bool wf, unit wf